$\forall$$a$,$b$:Id. ($\uparrow$eq\_id($a$; $b$)) $\Leftarrow\!\Rightarrow$ ($a$ = $b$)